((VARTYPECTR? . 3) (SAMELENGTH (NIL . (DECL (SL) (OT& (GROUND GROUND) . TRUTHVAL) CONSTANT) . NIL . ((SL . (CONSTANT . ((GROUND GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 1 . SL .))) . NIL . NIL . NIL . NIL . NIL . SAMELENGTH . NIL . NIL . 1 .) ((((∀ U V)) (≡ (SL U V) (∨ (∧ (NULL U) (NULL V)) (∧ (¬ (NULL U)) (¬ (NULL V)) (SL (CDR U) (CDR V)))))) . (AXIOM (TM& ((∀ U V)) (≡ (SL U V) (∨ (∧ (NULL U) (NULL V)) (∧ (∧ (¬ (NULL U)) (¬ (NULL V))) (SL (CDR U) (CDR V))))))) . NIL . ((NULL LISPAX . 8) (CDR LISPAX . 7) (V LISPAX . 1) (U LISPAX . 1) (SL . 1)) . NIL . NIL . NIL . (2) . NIL . SAMELENGTH . NIL . NIL . 2 .) ((((∀ V)) (≡ (SL U V) (∨ (∧ (NULL U) (NULL V)) (∧ (¬ (NULL U)) (¬ (NULL V)) (SL (CDR U) (CDR V)))))) . (∀E U (TM& . U) (LN& . 2) (MODE& STANDARD)) . NIL . ((NULL LISPAX . 8) (CDR LISPAX . 7) (V LISPAX . 1) (U LISPAX . 1) (SL . 1)) . NIL . NIL . NIL . (2) . NIL . SAMELENGTH . NIL . NIL . 3 .) ((≡ (SL U NNIL) (∨ (∧ (NULL U) (NULL NNIL)) (∧ (¬ (NULL U)) (¬ (NULL NNIL)) (SL (CDR U) (CDR NNIL))))) . (∀E V (TM& . NNIL) (LN& . 3) (MODE& STANDARD)) . NIL . ((NULL LISPAX . 8) (CDR LISPAX . 7) (U LISPAX . 1) (SL . 1) (NNIL LISPAX . 5)) . NIL . NIL . NIL . (2) . NIL . SAMELENGTH . NIL . NIL . 4 .) ((NULL NNIL) . (DECS (TM& NULL NNIL) (MODE& * ($ LINE (((∀ U)) (≡ (NULL U) (= U NNIL))) . 13) (STANDARD))) . NIL . ((NULL LISPAX . 8) (NNIL LISPAX . 5)) . NIL . NIL . NIL . ((LISPAX . 13)) . NIL . SAMELENGTH . NIL . NIL . 5 .) ((≡ (SL U NNIL) (= U NNIL)) . (DECS (TM& ≡ (SL U NNIL) (= U NNIL)) (MODE& * ($ LINE (((∀ U)) (≡ (NULL U) (= U NNIL))) . 13) (STANDARD)) (LR& 4 5)) . NIL . ((NNIL LISPAX . 5) (SL . 1) (U LISPAX . 1)) . NIL . NIL . NIL . ((LISPAX . 13) 2) . NIL . SAMELENGTH . NIL . NIL . 6 .) ((⊃ (∧ (SL NNIL NNIL) (((∀ X U)) (⊃ (SL U U) (SL (CONS X U) (CONS X U))))) (((∀ U)) (SL U U))) . (∀E PHI (TM& ((λ U)) (SL U U)) (LN& LISPAX . 17) (MODE& STANDARD) (LR& (LISPAX . 12))) . NIL . ((U LISPAX . 1) (X LISPAX . 2) (NNIL LISPAX . 5) (CONS LISPAX . 6) (SL . 1)) . NIL . NIL . NIL . ((LISPAX . 17) (LISPAX . 12)) . NIL . SAMELENGTH . NIL . NIL . 7 .) ((((∀ U)) (SL U U)) . (DECS (TM& ((∀ U)) (SL U U)) (MODE& STANDARD) (LR& 7 2 6 5) (LR&) (LR& (LISPAX . 12))) . NIL . ((SL . 1) (U LISPAX . 1)) . NIL . NIL . NIL . ((LISPAX . 12) (LISPAX . 13) 2 (LISPAX . 17)) . NIL . SAMELENGTH . NIL . NIL . 8 .) ((((∀ U)) (≡ (SL U NNIL) (= U NNIL))) . (∀I (U) (LN& . 6)) . NIL . ((NNIL LISPAX . 5) (SL . 1) (U LISPAX . 1)) . NIL . NIL . NIL . ((LISPAX . 13) 2) . NIL . SAMELENGTH . NIL . NIL . 9 .) ((⊃ (∧ (((∀ U X)) (⊃ (SL U NNIL) (SL (CONS X U) (* NNIL (LIST X))))) (((∀ X U)) (⊃ (((∀ U3 X)) (⊃ (SL U3 U) (SL (CONS X U3) (* U (LIST X))))) (((∀ U2 X1)) (⊃ (SL U2 (CONS X U)) (SL (CONS X1 U2) (* (CONS X U) (LIST X1)))))))) (((∀ U U1 X)) (⊃ (SL U1 U) (SL (CONS X U1) (* U (LIST X)))))) . (∀E PHI (TM& ((λ V)) (((∀ U X Y)) (⊃ (SL U V) (SL (CONS X U) (* V (LIST X)))))) (LN& LISPAX . 17) (MODE& STANDARD) (LR& (LISPAX . 12))) . NIL . ((U LISPAX . 1) (X LISPAX . 2) (NNIL LISPAX . 5) (CONS LISPAX . 6) (* LISPAX . 18) (SL . 1) (U1 . (VARIABLE . GROUND . LISTP . NIL . NIL . 10 . U1 .)) (U2 . (VARIABLE . GROUND . LISTP . NIL . NIL . 10 . U2 .)) (X1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 10 . X1 .)) (U3 . (VARIABLE . GROUND . LISTP . NIL . NIL . 10 . U3 .))) . ((LIST LISPAX . 22)) . NIL . NIL . ((LISPAX . 17) (LISPAX . 12)) . NIL . SAMELENGTH . NIL . NIL . 10 .) ((((∀ X U)) (⊃ (SL U NNIL) (= (CONS X U) (* NNIL (LIST X))))) . (DECS (TM& ((∀ X U)) (⊃ (SL U NNIL) (= (CONS X U) (* NNIL (LIST X))))) (MODE& STANDARD) (LR& 7 6 (LISPAX . 20) (LISPAX . 24)) (LR&) (LR& (LISPAX . 12) (LISPAX . 23) (LISPAX . 19))) . NIL . ((* LISPAX . 18) (SL . 1) (CONS LISPAX . 6) (NNIL LISPAX . 5) (X LISPAX . 2) (U LISPAX . 1)) . ((LIST LISPAX . 22)) . NIL . NIL . ((LISPAX . 19) (LISPAX . 23) (LISPAX . 12) (LISPAX . 24) (LISPAX . 20) 2 (LISPAX . 13) (LISPAX . 17)) . NIL . SAMELENGTH . NIL . NIL . 11 .) ((= U V) . (ASSUME (TM& = U V)) . NIL . ((V LISPAX . 1) (U LISPAX . 1)) . NIL . NIL . NIL . (12) . NIL . SAMELENGTH . NIL . NIL . 12 .) ((⊃ (((∀ U)) (SL U U)) (((∀ U V)) (⊃ (= U V) (SL U V)))) . (DEC (TM& ⊃ (((∀ U)) (SL U U)) (((∀ U V)) (⊃ (= U V) (SL U V))))) . NIL . ((V LISPAX . 1) (U LISPAX . 1) (SL . 1)) . NIL . NIL . NIL . NIL . NIL . SAMELENGTH . NIL . NIL . 13 .)) (LISPAX (NIL . (DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) (OT& . GROUND) VARIABLE LISTP) . NIL . ((W3 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . W3 .)) (W1 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . W1 .)) (W . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . W .)) (V2 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . V2 .)) (V0 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . V0 .)) (U3 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . U3 .)) (U1 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . U1 .)) (U . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . U .)) (LISTP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (5 . LISTP . PREFIX . 1000 .) . 1 . LISTP .)) (U0 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . U0 .)) (U2 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . U2 .)) (V . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . V .)) (V1 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . V1 .)) (V3 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . V3 .)) (W0 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . W0 .)) (W2 . (VARIABLE . GROUND . LISTP . NIL . NIL . 1 . W2 .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 1 .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Z .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . X .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 2 . SEXP .)) (Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Y .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 2 .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . C .)) (A . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . A .)) (B . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . B .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 3 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 4 . PHI .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 4 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LISTP) . NIL . ((NNIL . (CONSTANT . GROUND . LISTP . NIL . NIL . 5 . NNIL .)) (LISTP . 1)) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 6 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CDR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CDR .)) (CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CAR .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 7 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((NULL . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 8 . NULL .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 8 .) (NIL . (DECL (LISTP) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((LISTP . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 9 . LISTP .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 9 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((SEXP . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 10 . SEXP .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 10 .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U . 1) (SEXP . 10)) . NIL . NIL . NIL . (11) . NIL . LISPAX . NIL . NIL . 11 .) ((((∀ X U)) (LISTP (CONS X U))) . (AXIOM (TM& ((∀ X U)) (LISTP (CONS X U)))) . NIL . ((U . 1) (X . 2) (CONS . 6) (LISTP . 9)) . NIL . NIL . NIL . (12) . NIL . LISPAX . NIL . NIL . 12 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U . 1) (NNIL . 5) (NULL . 8)) . NIL . NIL . NIL . (13) . NIL . LISPAX . NIL . NIL . 13 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((U . 1) (X . 2) (CONS . 6) (NULL . 8)) . NIL . NIL . NIL . (14) . NIL . LISPAX . NIL . NIL . 14 .) ((((∀ X U)) (= (CAR (CONS X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (CONS X U)) X))) . NIL . ((U . 1) (X . 2) (CONS . 6) (CAR . 7)) . NIL . NIL . NIL . (15) . NIL . LISPAX . NIL . NIL . 15 .) ((((∀ X U)) (= (CDR (CONS X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (CONS X U)) U))) . NIL . ((U . 1) (X . 2) (CONS . 6) (CDR . 7)) . NIL . NIL . NIL . (16) . NIL . LISPAX . NIL . NIL . 16 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U))))) . NIL . ((U . 1) (X . 2) (PHI . 4) (NNIL . 5) (CONS . 6)) . NIL . NIL . NIL . (17) . NIL . LISPAX . NIL . NIL . 17 .) (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 840) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (1 . * . INFIX . 840 .) . 18 . * .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 18 .) ((((∀ U V)) (LISTP (* U V))) . (AXIOM (TM& ((∀ U V)) (LISTP (* U V)))) . NIL . ((V . 1) (U . 1) (LISTP . 9) (* . 18)) . NIL . NIL . NIL . (19) . NIL . LISPAX . NIL . NIL . 19 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((V . 1) (U . 1) (CONS . 6) (CAR . 7) (CDR . 7) (NULL . 8) (* . 18)) . NIL . NIL . NIL . (20) . NIL . LISPAX . NIL . NIL . 20 .) (NIL . (DECL (REVERSE LIST1) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((LIST1 . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 21 . LIST1 .)) (REVERSE . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 21 . REVERSE .))) . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 21 .) (NIL . (DECL (LIST) (FT& ((GROUND) GROUND NIL . GROUND)) FUNCTIONAL) . NIL . NIL . ((LIST . (FUNCTIONAL . (((GROUND) GROUND NIL . GROUND)) . UNIVERSAL . NIL . (4 . LIST . PREFIX . 1000 .) . 22 . LIST .))) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 22 .) ((((∀ X)) (LISTP (LIST X))) . (AXIOM (TM& ((∀ X)) (LISTP (LIST X)))) . NIL . ((X . 2) (LISTP . 9)) . ((LIST . 22)) . NIL . NIL . (23) . NIL . LISPAX . NIL . NIL . 23 .) ((((∀ X)) (= (LIST X) (CONS X NNIL))) . (AXIOM (TM& ((∀ X)) (= (LIST X) (CONS X NNIL)))) . NIL . ((X . 2) (NNIL . 5) (CONS . 6)) . ((LIST . 22)) . NIL . NIL . (24) . NIL . LISPAX . NIL . NIL . 24 .) ((((∀ X Y)) (LISTP (LIST X Y))) . (AXIOM (TM& ((∀ X Y)) (LISTP (LIST X Y)))) . NIL . ((Y . 2) (X . 2) (LISTP . 9)) . ((LIST . 22)) . NIL . NIL . (25) . NIL . LISPAX . NIL . NIL . 25 .) ((((∀ X Y)) (= (LIST X Y) (CONS X (LIST Y)))) . (AXIOM (TM& ((∀ X Y)) (= (LIST X Y) (CONS X (LIST Y))))) . NIL . ((Y . 2) (X . 2) (CONS . 6)) . ((LIST . 22)) . NIL . NIL . (26) . NIL . LISPAX . NIL . NIL . 26 .) ((((∀ X Y Z)) (LISTP (LIST X Y Z))) . (AXIOM (TM& ((∀ X Y Z)) (LISTP (LIST X Y Z)))) . NIL . ((Y . 2) (X . 2) (Z . 2) (LISTP . 9)) . ((LIST . 22)) . NIL . NIL . (27) . NIL . LISPAX . NIL . NIL . 27 .) ((((∀ X Y Z)) (= (LIST X Y Z) (CONS X (LIST Y Z)))) . (AXIOM (TM& ((∀ X Y Z)) (= (LIST X Y Z) (CONS X (LIST Y Z))))) . NIL . ((Y . 2) (X . 2) (Z . 2) (CONS . 6)) . ((LIST . 22)) . NIL . NIL . (28) . NIL . LISPAX . NIL . NIL . 28 .) ((((∀ U)) (LISTP (REVERSE U))) . (AXIOM (TM& ((∀ U)) (LISTP (REVERSE U)))) . NIL . ((U . 1) (LISTP . 9) (REVERSE . 21)) . NIL . NIL . NIL . (29) . NIL . LISPAX . NIL . NIL . 29 .) ((((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U)))))) . (AXIOM (TM& ((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U))))))) . NIL . ((U . 1) (NNIL . 5) (CAR . 7) (CDR . 7) (NULL . 8) (* . 18) (REVERSE . 21)) . ((LIST . 22)) . NIL . NIL . (30) . NIL . LISPAX . NIL . NIL . 30 .) ((((∀ U V W)) (= (* (* U V) W) (* U (* V W)))) . (AXIOM (TM& ((∀ U V W)) (= (* (* U V) W) (* U (* V W))))) . NIL . ((V . 1) (U . 1) (W . 1) (* . 18)) . NIL . NIL . NIL . (31) . NIL . LISPAX . NIL . NIL . 31 .) ((((∀ X U V)) (= (CONS X (* U V)) (* (CONS X U) V))) . (AXIOM (TM& ((∀ X U V)) (= (CONS X (* U V)) (* (CONS X U) V)))) . NIL . ((V . 1) (U . 1) (X . 2) (CONS . 6) (* . 18)) . NIL . NIL . NIL . (32) . NIL . LISPAX . NIL . NIL . 32 .) ((((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U)))) . (AXIOM (TM& ((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U))))) . NIL . ((V . 1) (U . 1) (* . 18) (REVERSE . 21)) . NIL . NIL . NIL . (33) . NIL . LISPAX . NIL . NIL . 33 .)) (SAMELE))